\section{Generating formulae} \label{generating_formulae}
Proving completeness or disjointness for a given pattern matching expression
means constructing a formula which represents that property, and proving its
validity using a theorem prover. \emph{Representing a property} means that we
have strong confidence that the formula will hold if and only if the property
is valid. This section explains the building process.

\subsection{General idea}
In the general sense, a pattern matching expression with $n$ patterns takes the following form:
\begin{lstlisting}
$s$ match {
    case $p_1$ $\Rightarrow$ $\ldots$
    case $p_2$ $\Rightarrow$ $\ldots$
    $\ldots$
    case $p_n$ $\Rightarrow$ $\ldots$
}
\end{lstlisting}

\begin{itemize}
\item Recall that it is \emph{complete}, if for any value of $s$, at least one
of the patterns $p_i$ matches it.  \item It is \emph{disjoint}, if for any
value of $s$, at most one of the patterns $p_i$ matches it. Informally, this
can thought as ``two patterns never overlap'', that is, the patterns are
\emph{pairwise disjoint}.
\end{itemize}

We want to generate formulae that represent these properties. Assume for a moment that for each pattern $p_i$ we can build a predicate $\xi(s, p_i)$ such that it holds if and only if the pattern $p_i$ matches the $s$. Straightforwardly, we would then have that the expression is:
\begin{itemize}
\item \emph{complete} if $\xi(s, p_1) \vee \xi(s, p_2) \vee \ldots \vee \xi(s, p_n)$ holds
\item \emph{disjoint} if $\neg(\xi(s, p_1) \wedge \xi(s, p_2)) \wedge \neg(\xi(s, p_1) \wedge \xi(s, p_3)) \wedge \ldots \wedge \neg(\xi(s, p_{n-1}) \wedge \xi(s, p_{n}))$ holds
\end{itemize}

We will now see in details how the predicates $\xi$ are constructed.

\subsection{Axioms}
Some information about a pattern matching expression is independent of the
patterns themselves. Examples of this are the class hierarchy structure, or the
type of the selector. These are \emph{axioms}, as they are always assumed to be
true and consitute the basis for our proofs of completeness or disjointness.
The formulae we presented above for these propreties hence take the following
forms, for $m$ axioms $a_1,\ldots , a_m$ and $n$ patterns $p_1,\ldots , p_n$:
\begin{itemize}
\item { \textbf{Completeness} \[\bigwedge_{k=1\ldots m} a_k \implies \bigvee_{i=1\ldots n} \xi{s, p_i}\] }

\item { \textbf{Disjointness} \[\bigwedge_{k=1\ldots m} a_k \implies \bigwedge_{
	\begin{array}{c}
	\mbox{\scriptsize $i=1\ldots n$}\\
	\mbox{\scriptsize $j=i+1\ldots n$}
	\end{array}} \neg(\xi(s, p_i) \wedge \xi(s, p_j))\] }
\end{itemize}

In this subsection, we go through the types of axioms we build.

\paragraph{Subtyping}
As formulae in the general sense are type-unaware, information about the class
hierarchy has to be represented somehow. For instance, the fact that subtypes
of a common supertype form a partition, is naturally very useful when it comes
to prove either completeness or disjointness of a given expression. Types are
encoded as sets. Type membership is hence naturally represented as set
membership, and subtyping as set inclusion.

Consider for instance the following hierarchy: 
\begin{lstlisting}
abstract class Tree
case class Node(left: Tree, right: Tree) extends Tree
case object Leaf extends Tree
\end{lstlisting}
We can make the following considerations:
\begin{itemize}
\item Any \textsf{Node} is a \textsf{Tree} and so is any \textsf{Leaf} (subtyping)
\item Any instance of \textsf{Tree} is either a \textsf{Node} or a \textsf{Leaf} (completeness of the subtypes)
\item A \textsf{Node} is never a \textsf{Leaf}, and vice versa (disjointness of the subtypes)
\end{itemize}

When it comes to building formulae, this gets encoded as follows:
\begin{itemize}
\item $Node \subset Tree \wedge Leaf \subset Tree$
\item $\forall t_0 \in Tree.t_0 \in Node \vee t_0 \in Leaf$
\item $\forall t_0 \in Tree.\neg(t_0 \in Node \wedge t_0 \in Leaf)$
\end{itemize}

\paragraph{Constructor parameters}
We explained how the subtyping relations of ADT are represented, but another
important information is the type of the constructor parameters. Continuing the
previous example, we can, informally, make some more observations:

\begin{itemize}
\item The left member of a \textsf{Node} is always of type \textsf{Tree}
\item So is the right member
\end{itemize}

Representing class members is somehow trickier, since we have to deal with the
recursive nature of algebraic data types; we could want to know the type of the
left member of the right member of the left member, etc., of a \textsf{Node}. The way we
go about this is by defining functions to ``extract'' class members. More
precisely, we define a new function for each class-member pair. Functions have
the nice property that, when applied to the same parameter, they always return
the same result. This properly represents the fact that any class member is
uniquely defined by its name and the instance from which it is extracted.

The observations above hence are represented as follows:
\begin{itemize}
\item $\forall n_0 \in Node.(\Psi_{(Node,left)}(n_0) \in Tree)$
\item $\forall n_0 \in Node.(\Psi_{(Node,right)}(n_0) \in Tree)$
\end{itemize}

It should be understood here that the entire expression $\Psi_{(Node,left)}$ is
nothing but a uniquely generated function name.

\paragraph{Objects}
We've mentioned that types are represented as sets. Objects are nothing but
special cases of classes, namely they are singletons. It is important that this
fact is properly encoded in the formulae, as comparison between two objects of
the same type should always be seen as equality. Perhaps not surprisingly, they
are simply represented as singleton sets. To complete the previous example, we
would hence also add the following: \begin{itemize}
\item $Leaf = \{ leaf_0 \}$
\end{itemize}

\paragraph{Type of the selector}
One last thing which is independent of the patterns is the type of the
selector. As previously mentioned, type membership is represented as set
membership, hence matching on a selector $t$ of type \textsf{Tree} will simply be
translated as $t \in Tree$.

\subsection{Translating patterns}
Thanks to the axioms we described in the previous subsection, there is only
little work left for translating the patterns themselves.

The pattern-specific predicates $\xi(s, p_i)$ are a conjunction of requirements
which have to hold for the given pattern $p_i$ to match the selector $s$. We
list here the properties we look into and the manner in which we encode them.

Consider the following pattern as an example:
\begin{lstlisting}
t match {
    $\ldots$
    case Node(Node(Leaf,_), r) if(r.isInstanceOf[Leaf])
      $\Rightarrow$ $\ldots$
    $\ldots$
}
\end{lstlisting}
Although it is written in a fairly unnatural way for a Scala programmer, it serves its purpose as an example of various constructs. 
					
\paragraph{\emph{Root} type}
We call the \emph{root} type of a pattern the outermost type to appear in it.
Obviously a required condition for a pattern to match the selector, is that its
root type should be the same as the selector's \emph{runtime} type, which will
be either the one it is declared to be, or one of its subtypes. In our example,
$t$ should be of type \textsf{Node} for the pattern to even have a chance to match it.
Thus, we would generate the following requirement:
\begin{itemize}
\item $t \in Node$
\end{itemize}

\paragraph{Members}
Restriction on members' types are encoded in a very similar way. Recall that we
use functions to represent class members. Therefore, the informal observations that
the left member of the \textsf{Node} we're matching on is itself a \textsf{Node} and that its
left member should be a \textsf{Leaf} are represented as follows:
\begin{itemize}
\item $\Psi_{(Node,left)}(t) \in Node$
\item $\Psi_{(Node,right)}(\Psi_{(Node,left)}(t)) \in Leaf$
\end{itemize}

\paragraph{Aliases}
Aliases are variables names which appear in the pattern. At runtime, the value
of the constructor parameter which they represent is bound to them, and the
aliases can thus be used in the code executed when the pattern is matched, or in
an additionnal guard, as in our example. To deal with them correctly, we first
generate a fresh variable name, then bind it to the proper class member using
the appropriate $\Psi$ function, and finally add the type constraint to our
fresh name. Notice that when no type is explicitely mentioned, we can simply
recover the most general one from the class structure. In our example, the $r$
alias is hence assumed to be of type \textsf{Tree}, and would be treated as follows:
\begin{itemize}
\item $r_{\text{\tiny{fresh}}} = \Psi_{(Node,right)}(t)$
\item $r_{\text{\tiny{fresh}}} \in Tree$ 
\end{itemize}
The first part is the binding to the class member. The way it is added to the
pattern formula differs whether we are trying to prove disjointness or
completeness of a formula:

\begin{itemize}
\item When trying to prove disjointness, we want to prove that, for each pair
of predicates $\xi(s, p_i)$ and $\xi(s, p_j)$, both cannot hold at the same
time. Thus, for each of these pairs, we write a formula in which we assume both
hold, and try to prove the negation of it. Intuitively, if a pattern matches
the selector, then the bindings have to be true. Thus, in the case of
disjunction, we can see the bindings as yet more constraints.

\item When trying to prove completeness, we cannot in general say that a
variable is bound to a given member. Indeed, it could be that the member
doesn't even exist. What we do instead is that we assume the bindings to be
true, and then try to prove that the rest of the constraints hold. Hence, we
can see the bindings as axioms holding for a given pattern. Following that
idea, all bindings are extracted and added in a conjunctive normal form as the
left-hand side of an implication whose right-hand side is the rest of the
pattern formula.
\end{itemize}

\paragraph{Wildcards}
Wildcards are encoded very straightforwardly. As, precisely, their goal is not
to add any constraints on a pattern, we can simply ignore them. Hence, in our
example, we do not add any restrictions on the value of the right member of the
left member of the selector. Had we had a pattern consisting only of a
wildcard, its corresponding formula would simply have been $true$.

\subsection{Translating guards}
Guards are perhaps the most interesting parts of a pattern when it comes to
proving completeness or disjointness of a complete expression. Indeed, they are
the most difficult part to deal with, as they can contain pretty much any code
which evaluates to a boolean. Obviously, we cannot in general statically
determine the outcome of any method call, hence, we need to come up with a
conservative approach. A very important simplification we make is that we
consider everything in the guards to be side-effect free.\footnotemark In
Scala, operators can be redefined and methods overloaded, but we make the
assumption that no one will reasonably want to do pattern-matching with
patterns affecting the state of the program.

\footnotetext{Our life would be much easier if Scala had a contract language,
	as we could rely on actual properties of methods rather than having to
			assume them. However, although such an extension is planned for
			future releases of Scala, it is not implemented yet.}

A guard on a pattern is essentially yet another restriction on the values which
will match it. Hence, the result of the translation of the guard into a formula
is simply ``and'ed'' to rest of the pattern formula.

The following can be extracted from guards:
\begin{itemize}
\item Conjunction and disjunction are kept ``as is''. Bitwise and lazy operators are treated indistinguishably.
\item Equality is conserved as long as both sides are simple identifiers or objects. The \texttt{.equals()} method is always assumed to be implemented correctly and is converted to a simple equality.
\item Operators and comparisons on primitive types are also kept ``as is''.
\item The generic \texttt{.isInstanceOf[\emph{type}]} method is translated into set membership.
\end{itemize}

Although this may seem to be a very loose way of approximating the guards, we believe it covers what Scala programmers write most of the time; range restrictions on primitive types, some dynamic type checking, comparison between members or objects, etc.
